Nuprl Definition : int_mul_mon
13,42
postcript
pdf
<
,*> == <
,
x
,
y
. (
x
=
y
),
x
,
y
.
x
z
y
,
x
,
y
.
x
*
y
, 1,
x
.
x
>
latex
Up
groups
1
Wellformedness Lemmas
int
mul
mon
wf
Definitions
(
i
=
j
)
,
i
z
j
origin
,*> == <, 
x,y. (x =
y), x,y. x 
z y, x,y. x * y, 1, x.x> ,*> == <, x,y. (x = y), x,y. x z y, x,y. x * y, 1, x.x> j)z j